es:ES, X:AbsInterface(Top), e:E.
((e  prior(X)))
 ((prior(X)(e) <loc e)
 & ((prior(X)(e)  X))
 & (e'':E. (e'' <loc e)  (prior(X)(e) <loc e'')  (((e''  X))))) 

latex

Definitions	x.A(x), e  X, ES, AbsInterface(A), Top, E, P  Q, P  Q, P & Q, x:A  B(x), b, x:A. B(x), x:AB(x)
Lemmas	es-local-pred-property, assert wf, es-E wf, es-interface wf, top wf, event system wf